$\forall$$M$:MsgA, $x$:Id, $s_{1}$, $s_{2}$:$M$.(timed)state.
\\[0ex]ma{-}x{-}tequiv($M$;$x$;$s_{1}$;$s_{2}$) $\Rightarrow$ (read{-}state($s_{1}$) $\equiv$ read{-}state($s_{2}$) mod $x$)